T:Type, L:T List, P, Q1, Q2:(||L||Prop), R:(||L||||L||Prop).
(i:||L||. Q2(i)  Q1(i))  causal_order(L;R;P;Q1)  causal_order(L;R;P;Q2) 

latex

Definitions	t  T, Prop, x:A. B(x), ||as||, {i..j}, P  Q, AB, P & Q, x:A. B(x), False, A, i  j < k, causal_order(L;R;P;Q)
Lemmas	le wf, int seg wf, length wf1